FDL - Step of Proof: bool-to-dcdr_wf

Step of Proof: bool-to-dcdr_wf

Inference at * 1
Iof proof for Lemma bool-to-dcdr wf:

1. A : Type
2. f : A

3. x : A

{f}

(x)

Dec(f(x) = tt)

by Assert {f}

(

x:A. Dec(f(x) = tt))

1: .....assertion..... NILNIL

1:

{f}

(

x:A. Dec(f(x) = tt))

2:

2: 4. {f}

(

x:A. Dec(f(x) = tt))

2:

{f}

(x)

Dec(f(x) = tt)

.

Definitions t T, x:A. B(x), Dec(P), s = t, , f(a), tt, {f}